(1
 (
  ("(var3 stable)" 0 96)
  ("(var3 up)" 96 98)
  ("(var3 down)" 98 100)
  ("(var3 up)" 100 128)
  ("(var3 stable)" 128 220)
  ("(var3 up)" 220 225)
  ("(var3 down)" 225 237)
  ("(var3 up)" 237 242)
  ("(var3 stable)" 242 387)
  ("(var3 up)" 387 389)
  ("(var3 down)" 389 391)
  ("(var4 stable)" 0 97)
  ("(var4 up)" 97 139)
  ("(var4 stable)" 139 391)
  ("(var1 stable)" 0 100)
  ("(var1 up)" 100 128)
  ("(var1 stable)" 128 391)
  ("(var2 stable)" 0 115)
  ("(var2 up)" 115 117)
  ("(var2 down)" 117 122)
  ("(var2 up)" 122 215)
  ("(var2 down)" 215 217)
  ("(var2 up)" 217 222)
  ("(var2 stable)" 222 224)
  ("(var2 up)" 224 270)
  ("(var2 down)" 270 272)
  ("(var2 up)" 272 274)
  ("(var2 stable)" 274 385)
  ("(var2 down)" 385 387)
  ("(var2 up)" 387 391)
 )
)
(2
 (
  ("(var3 stable)" 0 35)
  ("(var3 up)" 35 37)
  ("(var3 stable)" 37 41)
  ("(var3 up)" 41 68)
  ("(var3 stable)" 68 142)
  ("(var3 up)" 142 144)
  ("(var3 down)" 144 154)
  ("(var3 up)" 154 161)
  ("(var3 stable)" 161 283)
  ("(var4 stable)" 0 40)
  ("(var4 up)" 40 66)
  ("(var4 stable)" 66 283)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 70)
  ("(var1 stable)" 70 283)
  ("(var2 stable)" 0 52)
  ("(var2 up)" 52 54)
  ("(var2 down)" 54 59)
  ("(var2 up)" 59 190)
  ("(var2 stable)" 190 283)
 )
)
(3
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 92)
  ("(var3 stable)" 92 162)
  ("(var3 up)" 162 167)
  ("(var3 down)" 167 175)
  ("(var3 up)" 175 180)
  ("(var3 stable)" 180 308)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 91)
  ("(var4 stable)" 91 308)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 58)
  ("(var1 down)" 58 61)
  ("(var1 up)" 61 93)
  ("(var1 stable)" 93 308)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 84)
  ("(var2 stable)" 84 114)
  ("(var2 up)" 114 175)
  ("(var2 stable)" 175 308)
 )
)
(4
 (
  ("(var3 stable)" 0 83)
  ("(var3 up)" 83 118)
  ("(var3 stable)" 118 187)
  ("(var3 up)" 187 192)
  ("(var3 down)" 192 202)
  ("(var3 up)" 202 207)
  ("(var3 stable)" 207 328)
  ("(var4 stable)" 0 84)
  ("(var4 down)" 84 86)
  ("(var4 up)" 86 114)
  ("(var4 stable)" 114 328)
  ("(var1 stable)" 0 68)
  ("(var1 up)" 68 111)
  ("(var1 stable)" 111 328)
  ("(var2 stable)" 0 97)
  ("(var2 up)" 97 99)
  ("(var2 down)" 99 104)
  ("(var2 stable)" 104 138)
  ("(var2 up)" 138 140)
  ("(var2 down)" 140 143)
  ("(var2 up)" 143 222)
  ("(var2 stable)" 222 328)
 )
)
(5
 (
  ("(var3 stable)" 0 43)
  ("(var3 up)" 43 81)
  ("(var3 stable)" 81 161)
  ("(var3 up)" 161 164)
  ("(var3 stable)" 164 166)
  ("(var3 down)" 166 175)
  ("(var3 up)" 175 181)
  ("(var3 stable)" 181 317)
  ("(var4 stable)" 0 50)
  ("(var4 up)" 50 81)
  ("(var4 stable)" 81 317)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 82)
  ("(var1 stable)" 82 317)
  ("(var2 stable)" 0 64)
  ("(var2 up)" 64 66)
  ("(var2 down)" 66 71)
  ("(var2 up)" 71 205)
  ("(var2 stable)" 205 317)
 )
)
(6
 (
  ("(var3 stable)" 0 48)
  ("(var3 up)" 48 84)
  ("(var3 stable)" 84 173)
  ("(var3 up)" 173 177)
  ("(var3 down)" 177 188)
  ("(var3 up)" 188 193)
  ("(var3 stable)" 193 336)
  ("(var4 stable)" 0 49)
  ("(var4 up)" 49 84)
  ("(var4 stable)" 84 336)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 86)
  ("(var1 stable)" 86 336)
  ("(var2 stable)" 0 69)
  ("(var2 up)" 69 73)
  ("(var2 down)" 73 76)
  ("(var2 up)" 76 231)
  ("(var2 stable)" 231 336)
 )
)
(7
 (
  ("(var3 stable)" 0 36)
  ("(var3 up)" 36 73)
  ("(var3 stable)" 73 148)
  ("(var3 up)" 148 151)
  ("(var3 stable)" 151 153)
  ("(var3 down)" 153 162)
  ("(var3 up)" 162 167)
  ("(var3 stable)" 167 299)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 40)
  ("(var4 stable)" 40 42)
  ("(var4 up)" 42 68)
  ("(var4 stable)" 68 299)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 73)
  ("(var1 stable)" 73 299)
  ("(var2 stable)" 0 54)
  ("(var2 up)" 54 56)
  ("(var2 down)" 56 61)
  ("(var2 up)" 61 186)
  ("(var2 stable)" 186 299)
 )
)
(8
 (
  ("(var3 stable)" 0 73)
  ("(var3 up)" 73 98)
  ("(var3 stable)" 98 177)
  ("(var3 up)" 177 180)
  ("(var3 down)" 180 187)
  ("(var3 stable)" 187 318)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 97)
  ("(var4 stable)" 97 318)
  ("(var1 stable)" 0 67)
  ("(var1 up)" 67 70)
  ("(var1 stable)" 70 72)
  ("(var1 up)" 72 99)
  ("(var1 stable)" 99 318)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 87)
  ("(var2 down)" 87 91)
  ("(var2 up)" 91 216)
  ("(var2 stable)" 216 318)
 )
)
(9
 (
  ("(var3 stable)" 0 46)
  ("(var3 up)" 46 75)
  ("(var3 down)" 75 77)
  ("(var3 stable)" 77 157)
  ("(var3 up)" 157 163)
  ("(var3 down)" 163 173)
  ("(var3 up)" 173 179)
  ("(var3 stable)" 179 316)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 80)
  ("(var4 stable)" 80 82)
  ("(var4 up)" 82 84)
  ("(var4 stable)" 84 316)
  ("(var1 stable)" 0 43)
  ("(var1 up)" 43 80)
  ("(var1 stable)" 80 316)
  ("(var2 stable)" 0 61)
  ("(var2 up)" 61 63)
  ("(var2 down)" 63 68)
  ("(var2 up)" 68 188)
  ("(var2 stable)" 188 316)
 )
)
(10
 (
  ("(var3 stable)" 0 46)
  ("(var3 up)" 46 74)
  ("(var3 stable)" 74 166)
  ("(var3 up)" 166 172)
  ("(var3 down)" 172 182)
  ("(var3 stable)" 182 184)
  ("(var3 up)" 184 189)
  ("(var3 stable)" 189 337)
  ("(var4 stable)" 0 45)
  ("(var4 up)" 45 77)
  ("(var4 stable)" 77 337)
  ("(var1 stable)" 0 48)
  ("(var1 up)" 48 52)
  ("(var1 stable)" 52 54)
  ("(var1 up)" 54 76)
  ("(var1 stable)" 76 337)
  ("(var2 stable)" 0 61)
  ("(var2 up)" 61 63)
  ("(var2 down)" 63 68)
  ("(var2 stable)" 68 112)
  ("(var2 up)" 112 176)
  ("(var2 down)" 176 178)
  ("(var2 up)" 178 187)
  ("(var2 down)" 187 189)
  ("(var2 up)" 189 191)
  ("(var2 stable)" 191 337)
 )
)
(11
 (
  ("(var3 stable)" 0 93)
  ("(var3 up)" 93 133)
  ("(var3 stable)" 133 213)
  ("(var3 up)" 213 219)
  ("(var3 down)" 219 230)
  ("(var3 up)" 230 235)
  ("(var3 stable)" 235 379)
  ("(var4 stable)" 0 100)
  ("(var4 up)" 100 128)
  ("(var4 stable)" 128 379)
  ("(var1 stable)" 0 97)
  ("(var1 up)" 97 131)
  ("(var1 stable)" 131 379)
  ("(var2 stable)" 0 112)
  ("(var2 up)" 112 114)
  ("(var2 down)" 114 119)
  ("(var2 up)" 119 264)
  ("(var2 down)" 264 266)
  ("(var2 up)" 266 268)
  ("(var2 stable)" 268 379)
 )
)
(12
 (
  ("(var3 stable)" 0 81)
  ("(var3 down)" 81 83)
  ("(var3 up)" 83 105)
  ("(var3 stable)" 105 193)
  ("(var3 up)" 193 200)
  ("(var3 down)" 200 210)
  ("(var3 up)" 210 215)
  ("(var3 stable)" 215 354)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 73)
  ("(var4 stable)" 73 76)
  ("(var4 up)" 76 111)
  ("(var4 stable)" 111 354)
  ("(var1 stable)" 0 79)
  ("(var1 up)" 79 113)
  ("(var1 stable)" 113 354)
  ("(var2 stable)" 0 92)
  ("(var2 up)" 92 94)
  ("(var2 down)" 94 99)
  ("(var2 up)" 99 208)
  ("(var2 stable)" 208 354)
 )
)
(13
 (
  ("(var3 stable)" 0 98)
  ("(var3 up)" 98 130)
  ("(var3 stable)" 130 214)
  ("(var3 up)" 214 219)
  ("(var3 down)" 219 227)
  ("(var3 up)" 227 232)
  ("(var3 stable)" 232 375)
  ("(var4 stable)" 0 101)
  ("(var4 up)" 101 128)
  ("(var4 stable)" 128 375)
  ("(var1 stable)" 0 99)
  ("(var1 up)" 99 127)
  ("(var1 stable)" 127 375)
  ("(var2 stable)" 0 114)
  ("(var2 up)" 114 116)
  ("(var2 down)" 116 121)
  ("(var2 up)" 121 265)
  ("(var2 stable)" 265 375)
 )
)
(14
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 109)
  ("(var3 stable)" 109 200)
  ("(var3 up)" 200 206)
  ("(var3 down)" 206 215)
  ("(var3 up)" 215 221)
  ("(var3 stable)" 221 365)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 107)
  ("(var4 stable)" 107 365)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 106)
  ("(var1 stable)" 106 108)
  ("(var1 up)" 108 111)
  ("(var1 stable)" 111 365)
  ("(var2 stable)" 0 94)
  ("(var2 up)" 94 98)
  ("(var2 down)" 98 102)
  ("(var2 up)" 102 158)
  ("(var2 stable)" 158 160)
  ("(var2 up)" 160 196)
  ("(var2 down)" 196 198)
  ("(var2 up)" 198 228)
  ("(var2 down)" 228 230)
  ("(var2 up)" 230 233)
  ("(var2 down)" 233 235)
  ("(var2 stable)" 235 365)
 )
)
(15
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 105)
  ("(var3 stable)" 105 170)
  ("(var3 up)" 170 174)
  ("(var3 stable)" 174 176)
  ("(var3 down)" 176 184)
  ("(var3 up)" 184 187)
  ("(var3 stable)" 187 310)
  ("(var4 stable)" 0 72)
  ("(var4 up)" 72 74)
  ("(var4 stable)" 74 76)
  ("(var4 up)" 76 98)
  ("(var4 stable)" 98 310)
  ("(var1 stable)" 0 73)
  ("(var1 down)" 73 75)
  ("(var1 up)" 75 100)
  ("(var1 stable)" 100 310)
  ("(var2 stable)" 0 86)
  ("(var2 down)" 86 91)
  ("(var2 up)" 91 180)
  ("(var2 stable)" 180 183)
  ("(var2 up)" 183 190)
  ("(var2 stable)" 190 310)
 )
)
(16
 (
  ("(var3 stable)" 0 67)
  ("(var3 up)" 67 97)
  ("(var3 stable)" 97 172)
  ("(var3 up)" 172 176)
  ("(var3 down)" 176 185)
  ("(var3 up)" 185 190)
  ("(var3 stable)" 190 310)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 94)
  ("(var4 stable)" 94 96)
  ("(var4 up)" 96 98)
  ("(var4 stable)" 98 310)
  ("(var1 stable)" 0 72)
  ("(var1 up)" 72 100)
  ("(var1 stable)" 100 310)
  ("(var2 stable)" 0 84)
  ("(var2 up)" 84 257)
  ("(var2 stable)" 257 310)
 )
)
(17
 (
  ("(var3 stable)" 0 27)
  ("(var3 up)" 27 71)
  ("(var3 stable)" 71 142)
  ("(var3 up)" 142 147)
  ("(var3 down)" 147 156)
  ("(var3 stable)" 156 158)
  ("(var3 up)" 158 161)
  ("(var3 stable)" 161 295)
  ("(var4 stable)" 0 33)
  ("(var4 up)" 33 62)
  ("(var4 stable)" 62 295)
  ("(var1 stable)" 0 31)
  ("(var1 up)" 31 59)
  ("(var1 down)" 59 61)
  ("(var1 stable)" 61 295)
  ("(var2 stable)" 0 44)
  ("(var2 up)" 44 48)
  ("(var2 down)" 48 53)
  ("(var2 stable)" 53 97)
  ("(var2 up)" 97 176)
  ("(var2 stable)" 176 295)
 )
)
(18
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 97)
  ("(var3 stable)" 97 173)
  ("(var3 up)" 173 177)
  ("(var3 down)" 177 188)
  ("(var3 up)" 188 191)
  ("(var3 stable)" 191 325)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 92)
  ("(var4 stable)" 92 325)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 93)
  ("(var1 stable)" 93 325)
  ("(var2 stable)" 0 79)
  ("(var2 up)" 79 81)
  ("(var2 down)" 81 86)
  ("(var2 up)" 86 218)
  ("(var2 stable)" 218 325)
 )
)
(19
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 94)
  ("(var3 stable)" 94 179)
  ("(var3 up)" 179 184)
  ("(var3 down)" 184 195)
  ("(var3 up)" 195 200)
  ("(var3 stable)" 200 334)
  ("(var4 stable)" 0 66)
  ("(var4 up)" 66 100)
  ("(var4 stable)" 100 334)
  ("(var1 stable)" 0 64)
  ("(var1 up)" 64 96)
  ("(var1 stable)" 96 334)
  ("(var2 stable)" 0 83)
  ("(var2 up)" 83 85)
  ("(var2 down)" 85 90)
  ("(var2 up)" 90 209)
  ("(var2 down)" 209 211)
  ("(var2 up)" 211 213)
  ("(var2 stable)" 213 334)
 )
)
(20
 (
  ("(var3 stable)" 0 31)
  ("(var3 up)" 31 66)
  ("(var3 stable)" 66 137)
  ("(var3 up)" 137 141)
  ("(var3 down)" 141 151)
  ("(var3 up)" 151 156)
  ("(var3 stable)" 156 278)
  ("(var4 stable)" 0 35)
  ("(var4 up)" 35 64)
  ("(var4 stable)" 64 278)
  ("(var1 stable)" 0 32)
  ("(var1 up)" 32 70)
  ("(var1 stable)" 70 278)
  ("(var2 stable)" 0 46)
  ("(var2 up)" 46 50)
  ("(var2 down)" 50 54)
  ("(var2 up)" 54 178)
  ("(var2 stable)" 178 278)
 )
)
(21
 (
  ("(var3 stable)" 0 60)
  ("(var3 up)" 60 101)
  ("(var3 stable)" 101 172)
  ("(var3 up)" 172 178)
  ("(var3 down)" 178 189)
  ("(var3 up)" 189 191)
  ("(var3 stable)" 191 328)
  ("(var4 stable)" 0 53)
  ("(var4 up)" 53 55)
  ("(var4 down)" 55 57)
  ("(var4 up)" 57 61)
  ("(var4 stable)" 61 63)
  ("(var4 up)" 63 91)
  ("(var4 stable)" 91 328)
  ("(var1 stable)" 0 58)
  ("(var1 up)" 58 90)
  ("(var1 stable)" 90 328)
  ("(var2 stable)" 0 74)
  ("(var2 up)" 74 78)
  ("(var2 down)" 78 83)
  ("(var2 up)" 83 182)
  ("(var2 down)" 182 184)
  ("(var2 up)" 184 187)
  ("(var2 down)" 187 189)
  ("(var2 up)" 189 216)
  ("(var2 stable)" 216 328)
 )
)
(22
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 66)
  ("(var3 down)" 66 68)
  ("(var3 up)" 68 101)
  ("(var3 stable)" 101 185)
  ("(var3 up)" 185 190)
  ("(var3 down)" 190 203)
  ("(var3 up)" 203 209)
  ("(var3 down)" 209 211)
  ("(var3 stable)" 211 353)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 100)
  ("(var4 stable)" 100 353)
  ("(var1 stable)" 0 59)
  ("(var1 up)" 59 99)
  ("(var1 stable)" 99 353)
  ("(var2 stable)" 0 83)
  ("(var2 up)" 83 86)
  ("(var2 down)" 86 90)
  ("(var2 up)" 90 230)
  ("(var2 down)" 230 233)
  ("(var2 stable)" 233 353)
 )
)
(23
 (
  ("(var3 stable)" 0 98)
  ("(var3 up)" 98 134)
  ("(var3 stable)" 134 215)
  ("(var3 up)" 215 223)
  ("(var3 down)" 223 234)
  ("(var3 up)" 234 240)
  ("(var3 stable)" 240 385)
  ("(var4 stable)" 0 100)
  ("(var4 up)" 100 133)
  ("(var4 stable)" 133 385)
  ("(var1 stable)" 0 99)
  ("(var1 up)" 99 133)
  ("(var1 stable)" 133 385)
  ("(var2 stable)" 0 114)
  ("(var2 up)" 114 116)
  ("(var2 down)" 116 121)
  ("(var2 stable)" 121 165)
  ("(var2 up)" 165 273)
  ("(var2 stable)" 273 385)
 )
)
(24
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 117)
  ("(var3 stable)" 117 197)
  ("(var3 up)" 197 205)
  ("(var3 down)" 205 216)
  ("(var3 up)" 216 221)
  ("(var3 stable)" 221 362)
  ("(var4 stable)" 0 82)
  ("(var4 up)" 82 94)
  ("(var4 stable)" 94 96)
  ("(var4 up)" 96 107)
  ("(var4 down)" 107 109)
  ("(var4 up)" 109 111)
  ("(var4 stable)" 111 362)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 109)
  ("(var1 stable)" 109 362)
  ("(var2 stable)" 0 94)
  ("(var2 up)" 94 97)
  ("(var2 down)" 97 101)
  ("(var2 stable)" 101 150)
  ("(var2 up)" 150 230)
  ("(var2 down)" 230 232)
  ("(var2 up)" 232 234)
  ("(var2 stable)" 234 362)
 )
)
(25
 (
  ("(var3 stable)" 0 54)
  ("(var3 up)" 54 59)
  ("(var3 down)" 59 61)
  ("(var3 up)" 61 86)
  ("(var3 stable)" 86 172)
  ("(var3 up)" 172 176)
  ("(var3 down)" 176 185)
  ("(var3 stable)" 185 187)
  ("(var3 up)" 187 190)
  ("(var3 stable)" 190 326)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 92)
  ("(var4 down)" 92 94)
  ("(var4 stable)" 94 326)
  ("(var1 stable)" 0 52)
  ("(var1 down)" 52 54)
  ("(var1 up)" 54 95)
  ("(var1 stable)" 95 326)
  ("(var2 stable)" 0 73)
  ("(var2 up)" 73 75)
  ("(var2 down)" 75 80)
  ("(var2 up)" 80 205)
  ("(var2 down)" 205 208)
  ("(var2 stable)" 208 326)
 )
)
(26
 (
  ("(var3 stable)" 0 77)
  ("(var3 down)" 77 79)
  ("(var3 up)" 79 107)
  ("(var3 down)" 107 109)
  ("(var3 up)" 109 111)
  ("(var3 stable)" 111 179)
  ("(var3 up)" 179 185)
  ("(var3 down)" 185 195)
  ("(var3 up)" 195 198)
  ("(var3 stable)" 198 323)
  ("(var4 stable)" 0 79)
  ("(var4 up)" 79 106)
  ("(var4 stable)" 106 323)
  ("(var1 stable)" 0 81)
  ("(var1 up)" 81 107)
  ("(var1 stable)" 107 323)
  ("(var2 stable)" 0 92)
  ("(var2 up)" 92 94)
  ("(var2 down)" 94 98)
  ("(var2 up)" 98 187)
  ("(var2 stable)" 187 189)
  ("(var2 up)" 189 226)
  ("(var2 stable)" 226 323)
 )
)
(27
 (
  ("(var3 stable)" 0 44)
  ("(var3 up)" 44 69)
  ("(var3 stable)" 69 145)
  ("(var3 up)" 145 149)
  ("(var3 down)" 149 158)
  ("(var3 up)" 158 164)
  ("(var3 stable)" 164 295)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 75)
  ("(var4 stable)" 75 295)
  ("(var1 stable)" 0 41)
  ("(var1 up)" 41 44)
  ("(var1 stable)" 44 46)
  ("(var1 up)" 46 70)
  ("(var1 stable)" 70 295)
  ("(var2 stable)" 0 54)
  ("(var2 up)" 54 56)
  ("(var2 down)" 56 61)
  ("(var2 up)" 61 185)
  ("(var2 stable)" 185 295)
 )
)
(28
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 64)
  ("(var3 stable)" 64 66)
  ("(var3 up)" 66 68)
  ("(var3 stable)" 68 148)
  ("(var3 up)" 148 153)
  ("(var3 down)" 153 161)
  ("(var3 up)" 161 166)
  ("(var3 stable)" 166 303)
  ("(var4 stable)" 0 39)
  ("(var4 up)" 39 66)
  ("(var4 down)" 66 68)
  ("(var4 stable)" 68 303)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 66)
  ("(var1 stable)" 66 303)
  ("(var2 stable)" 0 51)
  ("(var2 up)" 51 53)
  ("(var2 down)" 53 58)
  ("(var2 stable)" 58 101)
  ("(var2 up)" 101 192)
  ("(var2 stable)" 192 303)
 )
)
(29
 (
  ("(var3 stable)" 0 66)
  ("(var3 up)" 66 102)
  ("(var3 stable)" 102 177)
  ("(var3 up)" 177 185)
  ("(var3 down)" 185 194)
  ("(var3 up)" 194 202)
  ("(var3 stable)" 202 334)
  ("(var4 stable)" 0 61)
  ("(var4 up)" 61 95)
  ("(var4 stable)" 95 334)
  ("(var1 up)" 0 2)
  ("(var1 stable)" 2 68)
  ("(var1 up)" 68 94)
  ("(var1 stable)" 94 334)
  ("(var2 stable)" 0 81)
  ("(var2 up)" 81 83)
  ("(var2 down)" 83 88)
  ("(var2 up)" 88 218)
  ("(var2 stable)" 218 334)
 )
)
(30
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 104)
  ("(var3 stable)" 104 176)
  ("(var3 up)" 176 180)
  ("(var3 down)" 180 188)
  ("(var3 stable)" 188 190)
  ("(var3 up)" 190 193)
  ("(var3 stable)" 193 315)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 99)
  ("(var4 down)" 99 101)
  ("(var4 up)" 101 103)
  ("(var4 stable)" 103 315)
  ("(var1 stable)" 0 60)
  ("(var1 up)" 60 104)
  ("(var1 stable)" 104 315)
  ("(var2 stable)" 0 86)
  ("(var2 up)" 86 88)
  ("(var2 down)" 88 93)
  ("(var2 up)" 93 215)
  ("(var2 stable)" 215 315)
 )
)
(31
 (
  ("(var3 stable)" 0 89)
  ("(var3 up)" 89 124)
  ("(var3 stable)" 124 203)
  ("(var3 up)" 203 210)
  ("(var3 down)" 210 220)
  ("(var3 up)" 220 225)
  ("(var3 down)" 225 227)
  ("(var3 stable)" 227 364)
  ("(var4 stable)" 0 82)
  ("(var4 up)" 82 123)
  ("(var4 stable)" 123 364)
  ("(var1 stable)" 0 93)
  ("(var1 up)" 93 124)
  ("(var1 stable)" 124 364)
  ("(var2 stable)" 0 105)
  ("(var2 up)" 105 109)
  ("(var2 down)" 109 114)
  ("(var2 up)" 114 241)
  ("(var2 stable)" 241 364)
 )
)
(32
 (
  ("(var3 stable)" 0 33)
  ("(var3 up)" 33 35)
  ("(var3 stable)" 35 37)
  ("(var3 up)" 37 62)
  ("(var3 stable)" 62 142)
  ("(var3 up)" 142 146)
  ("(var3 down)" 146 156)
  ("(var3 stable)" 156 158)
  ("(var3 up)" 158 162)
  ("(var3 stable)" 162 295)
  ("(var4 stable)" 0 30)
  ("(var4 up)" 30 63)
  ("(var4 stable)" 63 295)
  ("(var1 stable)" 0 32)
  ("(var1 up)" 32 71)
  ("(var1 stable)" 71 295)
  ("(var2 stable)" 0 48)
  ("(var2 up)" 48 50)
  ("(var2 down)" 50 55)
  ("(var2 up)" 55 179)
  ("(var2 stable)" 179 293)
  ("(var2 down)" 293 295)
 )
)
(33
 (
  ("(var3 stable)" 0 62)
  ("(var3 up)" 62 86)
  ("(var3 stable)" 86 159)
  ("(var3 up)" 159 163)
  ("(var3 stable)" 163 165)
  ("(var3 down)" 165 174)
  ("(var3 stable)" 174 292)
  ("(var4 stable)" 0 54)
  ("(var4 up)" 54 56)
  ("(var4 stable)" 56 59)
  ("(var4 up)" 59 83)
  ("(var4 stable)" 83 292)
  ("(var1 stable)" 0 58)
  ("(var1 up)" 58 83)
  ("(var1 stable)" 83 292)
  ("(var2 stable)" 0 70)
  ("(var2 up)" 70 76)
  ("(var2 down)" 76 78)
  ("(var2 up)" 78 186)
  ("(var2 stable)" 186 292)
 )
)
(34
 (
  ("(var3 stable)" 0 48)
  ("(var3 up)" 48 85)
  ("(var3 stable)" 85 167)
  ("(var3 up)" 167 173)
  ("(var3 down)" 173 182)
  ("(var3 up)" 182 187)
  ("(var3 stable)" 187 329)
  ("(var4 stable)" 0 50)
  ("(var4 up)" 50 81)
  ("(var4 stable)" 81 329)
  ("(var1 stable)" 0 49)
  ("(var1 up)" 49 84)
  ("(var1 stable)" 84 329)
  ("(var2 stable)" 0 64)
  ("(var2 up)" 64 68)
  ("(var2 down)" 68 72)
  ("(var2 up)" 72 227)
  ("(var2 stable)" 227 329)
 )
)
(35
 (
  ("(var3 stable)" 0 33)
  ("(var3 down)" 33 35)
  ("(var3 up)" 35 62)
  ("(var3 stable)" 62 64)
  ("(var3 up)" 64 67)
  ("(var3 stable)" 67 131)
  ("(var3 up)" 131 135)
  ("(var3 down)" 135 147)
  ("(var3 up)" 147 151)
  ("(var3 stable)" 151 271)
  ("(var4 stable)" 0 29)
  ("(var4 up)" 29 62)
  ("(var4 stable)" 62 271)
  ("(var1 stable)" 0 28)
  ("(var1 up)" 28 67)
  ("(var1 stable)" 67 271)
  ("(var2 stable)" 0 48)
  ("(var2 up)" 48 50)
  ("(var2 down)" 50 53)
  ("(var2 up)" 53 209)
  ("(var2 stable)" 209 271)
 )
)
(36
 (
  ("(var3 up)" 0 3)
  ("(var3 down)" 3 5)
  ("(var3 stable)" 5 61)
  ("(var3 up)" 61 94)
  ("(var3 stable)" 94 183)
  ("(var3 up)" 183 186)
  ("(var3 stable)" 186 188)
  ("(var3 down)" 188 197)
  ("(var3 up)" 197 199)
  ("(var3 stable)" 199 347)
  ("(var4 stable)" 0 63)
  ("(var4 up)" 63 96)
  ("(var4 stable)" 96 347)
  ("(var1 stable)" 0 52)
  ("(var1 down)" 52 54)
  ("(var1 up)" 54 101)
  ("(var1 stable)" 101 347)
  ("(var2 stable)" 0 78)
  ("(var2 up)" 78 80)
  ("(var2 down)" 80 85)
  ("(var2 up)" 85 221)
  ("(var2 stable)" 221 347)
 )
)
(37
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 94)
  ("(var3 stable)" 94 168)
  ("(var3 up)" 168 173)
  ("(var3 down)" 173 183)
  ("(var3 up)" 183 187)
  ("(var3 stable)" 187 313)
  ("(var4 stable)" 0 67)
  ("(var4 down)" 67 69)
  ("(var4 up)" 69 97)
  ("(var4 stable)" 97 313)
  ("(var1 stable)" 0 64)
  ("(var1 up)" 64 92)
  ("(var1 stable)" 92 313)
  ("(var2 stable)" 0 81)
  ("(var2 up)" 81 83)
  ("(var2 down)" 83 87)
  ("(var2 up)" 87 200)
  ("(var2 down)" 200 202)
  ("(var2 up)" 202 206)
  ("(var2 stable)" 206 313)
 )
)
(38
 (
  ("(var3 stable)" 0 81)
  ("(var3 up)" 81 85)
  ("(var3 down)" 85 87)
  ("(var3 up)" 87 113)
  ("(var3 down)" 113 116)
  ("(var3 up)" 116 118)
  ("(var3 stable)" 118 203)
  ("(var3 up)" 203 207)
  ("(var3 down)" 207 219)
  ("(var3 up)" 219 224)
  ("(var3 stable)" 224 365)
  ("(var4 stable)" 0 84)
  ("(var4 down)" 84 86)
  ("(var4 up)" 86 118)
  ("(var4 stable)" 118 365)
  ("(var1 stable)" 0 81)
  ("(var1 down)" 81 83)
  ("(var1 up)" 83 85)
  ("(var1 stable)" 85 87)
  ("(var1 up)" 87 116)
  ("(var1 stable)" 116 365)
  ("(var2 stable)" 0 100)
  ("(var2 up)" 100 102)
  ("(var2 down)" 102 107)
  ("(var2 up)" 107 219)
  ("(var2 stable)" 219 365)
 )
)
(39
 (
  ("(var3 stable)" 0 69)
  ("(var3 up)" 69 97)
  ("(var3 stable)" 97 177)
  ("(var3 up)" 177 181)
  ("(var3 down)" 181 191)
  ("(var3 up)" 191 198)
  ("(var3 down)" 198 200)
  ("(var3 stable)" 200 329)
  ("(var4 stable)" 0 60)
  ("(var4 up)" 60 96)
  ("(var4 stable)" 96 329)
  ("(var1 stable)" 0 67)
  ("(var1 up)" 67 93)
  ("(var1 stable)" 93 95)
  ("(var1 up)" 95 100)
  ("(var1 stable)" 100 102)
  ("(var1 up)" 102 105)
  ("(var1 stable)" 105 329)
  ("(var2 stable)" 0 82)
  ("(var2 up)" 82 84)
  ("(var2 down)" 84 89)
  ("(var2 stable)" 89 132)
  ("(var2 up)" 132 224)
  ("(var2 stable)" 224 329)
 )
)
(40
 (
  ("(var3 stable)" 0 33)
  ("(var3 up)" 33 63)
  ("(var3 stable)" 63 141)
  ("(var3 up)" 141 145)
  ("(var3 down)" 145 155)
  ("(var3 up)" 155 158)
  ("(var3 stable)" 158 285)
  ("(var4 stable)" 0 32)
  ("(var4 up)" 32 36)
  ("(var4 down)" 36 38)
  ("(var4 up)" 38 70)
  ("(var4 stable)" 70 285)
  ("(var1 stable)" 0 36)
  ("(var1 up)" 36 65)
  ("(var1 stable)" 65 285)
  ("(var2 stable)" 0 46)
  ("(var2 up)" 46 50)
  ("(var2 down)" 50 54)
  ("(var2 up)" 54 171)
  ("(var2 stable)" 171 285)
 )
)
(41
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 82)
  ("(var3 stable)" 82 155)
  ("(var3 up)" 155 159)
  ("(var3 down)" 159 163)
  ("(var3 stable)" 163 301)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 76)
  ("(var4 stable)" 76 301)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 79)
  ("(var1 stable)" 79 301)
  ("(var2 stable)" 0 62)
  ("(var2 up)" 62 64)
  ("(var2 down)" 64 69)
  ("(var2 stable)" 69 111)
  ("(var2 up)" 111 171)
  ("(var2 down)" 171 173)
  ("(var2 up)" 173 175)
  ("(var2 stable)" 175 301)
 )
)
(42
 (
  ("(var3 stable)" 0 49)
  ("(var3 up)" 49 84)
  ("(var3 stable)" 84 168)
  ("(var3 up)" 168 172)
  ("(var3 down)" 172 182)
  ("(var3 up)" 182 187)
  ("(var3 stable)" 187 323)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 86)
  ("(var4 stable)" 86 323)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 86)
  ("(var1 stable)" 86 323)
  ("(var2 stable)" 0 69)
  ("(var2 up)" 69 71)
  ("(var2 down)" 71 76)
  ("(var2 up)" 76 199)
  ("(var2 stable)" 199 323)
 )
)
(43
 (
  ("(var3 stable)" 0 62)
  ("(var3 up)" 62 99)
  ("(var3 stable)" 99 175)
  ("(var3 up)" 175 182)
  ("(var3 down)" 182 192)
  ("(var3 up)" 192 196)
  ("(var3 stable)" 196 330)
  ("(var4 stable)" 0 58)
  ("(var4 up)" 58 95)
  ("(var4 stable)" 95 330)
  ("(var1 stable)" 0 62)
  ("(var1 up)" 62 93)
  ("(var1 stable)" 93 330)
  ("(var2 stable)" 0 80)
  ("(var2 up)" 80 82)
  ("(var2 down)" 82 87)
  ("(var2 up)" 87 213)
  ("(var2 down)" 213 219)
  ("(var2 stable)" 219 330)
 )
)
(44
 (
  ("(var3 stable)" 0 46)
  ("(var3 up)" 46 76)
  ("(var3 stable)" 76 169)
  ("(var3 up)" 169 174)
  ("(var3 down)" 174 184)
  ("(var3 up)" 184 189)
  ("(var3 stable)" 189 328)
  ("(var4 stable)" 0 41)
  ("(var4 up)" 41 72)
  ("(var4 stable)" 72 328)
  ("(var1 stable)" 0 46)
  ("(var1 up)" 46 81)
  ("(var1 stable)" 81 328)
  ("(var2 stable)" 0 62)
  ("(var2 up)" 62 66)
  ("(var2 down)" 66 70)
  ("(var2 stable)" 70 118)
  ("(var2 up)" 118 208)
  ("(var2 stable)" 208 210)
  ("(var2 down)" 210 212)
  ("(var2 stable)" 212 328)
 )
)
(45
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 87)
  ("(var3 down)" 87 89)
  ("(var3 stable)" 89 176)
  ("(var3 up)" 176 183)
  ("(var3 down)" 183 194)
  ("(var3 up)" 194 200)
  ("(var3 stable)" 200 347)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 95)
  ("(var4 stable)" 95 347)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 85)
  ("(var1 stable)" 85 87)
  ("(var1 up)" 87 89)
  ("(var1 stable)" 89 347)
  ("(var2 stable)" 0 70)
  ("(var2 up)" 70 72)
  ("(var2 down)" 72 77)
  ("(var2 up)" 77 222)
  ("(var2 stable)" 222 347)
 )
)
(46
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 98)
  ("(var3 stable)" 98 178)
  ("(var3 up)" 178 182)
  ("(var3 down)" 182 192)
  ("(var3 up)" 192 200)
  ("(var3 stable)" 200 337)
  ("(var4 stable)" 0 58)
  ("(var4 up)" 58 94)
  ("(var4 down)" 94 97)
  ("(var4 up)" 97 99)
  ("(var4 stable)" 99 337)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 59)
  ("(var1 stable)" 59 63)
  ("(var1 up)" 63 95)
  ("(var1 stable)" 95 337)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 79)
  ("(var2 down)" 79 84)
  ("(var2 up)" 84 194)
  ("(var2 stable)" 194 228)
  ("(var2 down)" 228 230)
  ("(var2 up)" 230 232)
  ("(var2 stable)" 232 337)
 )
)
(47
 (
  ("(var3 stable)" 0 67)
  ("(var3 up)" 67 96)
  ("(var3 stable)" 96 164)
  ("(var3 up)" 164 170)
  ("(var3 down)" 170 179)
  ("(var3 up)" 179 181)
  ("(var3 stable)" 181 309)
  ("(var4 stable)" 0 68)
  ("(var4 up)" 68 88)
  ("(var4 stable)" 88 309)
  ("(var1 stable)" 0 66)
  ("(var1 up)" 66 90)
  ("(var1 stable)" 90 309)
  ("(var2 stable)" 0 76)
  ("(var2 up)" 76 78)
  ("(var2 down)" 78 82)
  ("(var2 up)" 82 207)
  ("(var2 down)" 207 209)
  ("(var2 up)" 209 211)
  ("(var2 stable)" 211 309)
 )
)
(48
 (
  ("(var3 stable)" 0 88)
  ("(var3 up)" 88 122)
  ("(var3 stable)" 122 195)
  ("(var3 up)" 195 201)
  ("(var3 down)" 201 211)
  ("(var3 up)" 211 217)
  ("(var3 stable)" 217 348)
  ("(var4 stable)" 0 86)
  ("(var4 up)" 86 119)
  ("(var4 stable)" 119 348)
  ("(var1 stable)" 0 77)
  ("(var1 up)" 77 123)
  ("(var1 stable)" 123 348)
  ("(var2 stable)" 0 102)
  ("(var2 up)" 102 104)
  ("(var2 down)" 104 109)
  ("(var2 stable)" 109 151)
  ("(var2 up)" 151 238)
  ("(var2 stable)" 238 348)
 )
)
(49
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 99)
  ("(var3 stable)" 99 180)
  ("(var3 up)" 180 185)
  ("(var3 down)" 185 195)
  ("(var3 up)" 195 199)
  ("(var3 stable)" 199 332)
  ("(var4 stable)" 0 71)
  ("(var4 up)" 71 98)
  ("(var4 stable)" 98 332)
  ("(var1 stable)" 0 66)
  ("(var1 up)" 66 99)
  ("(var1 stable)" 99 332)
  ("(var2 stable)" 0 84)
  ("(var2 up)" 84 86)
  ("(var2 down)" 86 91)
  ("(var2 up)" 91 189)
  ("(var2 stable)" 189 191)
  ("(var2 up)" 191 226)
  ("(var2 stable)" 226 332)
 )
)
(50
 (
  ("(var3 stable)" 0 53)
  ("(var3 up)" 53 98)
  ("(var3 stable)" 98 170)
  ("(var3 up)" 170 175)
  ("(var3 down)" 175 184)
  ("(var3 stable)" 184 186)
  ("(var3 up)" 186 189)
  ("(var3 stable)" 189 327)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 86)
  ("(var4 stable)" 86 327)
  ("(var1 stable)" 0 57)
  ("(var1 up)" 57 92)
  ("(var1 stable)" 92 327)
  ("(var2 stable)" 0 72)
  ("(var2 up)" 72 74)
  ("(var2 down)" 74 79)
  ("(var2 up)" 79 212)
  ("(var2 stable)" 212 327)
 )
)
(51
 (
  ("(var3 stable)" 0 53)
  ("(var3 up)" 53 91)
  ("(var3 stable)" 91 178)
  ("(var3 up)" 178 183)
  ("(var3 down)" 183 194)
  ("(var3 up)" 194 199)
  ("(var3 stable)" 199 336)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 92)
  ("(var4 stable)" 92 336)
  ("(var1 stable)" 0 57)
  ("(var1 up)" 57 89)
  ("(var1 stable)" 89 336)
  ("(var2 stable)" 0 72)
  ("(var2 up)" 72 77)
  ("(var2 down)" 77 81)
  ("(var2 up)" 81 223)
  ("(var2 stable)" 223 336)
 )
)
(52
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 81)
  ("(var3 stable)" 81 158)
  ("(var3 up)" 158 162)
  ("(var3 down)" 162 173)
  ("(var3 up)" 173 175)
  ("(var3 stable)" 175 301)
  ("(var4 stable)" 0 55)
  ("(var4 up)" 55 81)
  ("(var4 stable)" 81 301)
  ("(var1 stable)" 0 58)
  ("(var1 up)" 58 80)
  ("(var1 stable)" 80 301)
  ("(var2 stable)" 0 68)
  ("(var2 up)" 68 70)
  ("(var2 down)" 70 74)
  ("(var2 up)" 74 162)
  ("(var2 stable)" 162 164)
  ("(var2 up)" 164 212)
  ("(var2 stable)" 212 301)
 )
)
(53
 (
  ("(var3 stable)" 0 39)
  ("(var3 up)" 39 67)
  ("(var3 stable)" 67 147)
  ("(var3 up)" 147 153)
  ("(var3 down)" 153 162)
  ("(var3 up)" 162 167)
  ("(var3 stable)" 167 302)
  ("(var4 stable)" 0 26)
  ("(var4 up)" 26 65)
  ("(var4 stable)" 65 302)
  ("(var1 stable)" 0 34)
  ("(var1 up)" 34 66)
  ("(var1 stable)" 66 302)
  ("(var2 stable)" 0 50)
  ("(var2 up)" 50 52)
  ("(var2 down)" 52 57)
  ("(var2 stable)" 57 101)
  ("(var2 up)" 101 184)
  ("(var2 stable)" 184 302)
 )
)
(54
 (
  ("(var3 up)" 0 2)
  ("(var3 stable)" 2 96)
  ("(var3 up)" 96 98)
  ("(var3 stable)" 98 101)
  ("(var3 up)" 101 135)
  ("(var3 stable)" 135 221)
  ("(var3 up)" 221 225)
  ("(var3 down)" 225 236)
  ("(var3 up)" 236 242)
  ("(var3 stable)" 242 391)
  ("(var4 stable)" 0 100)
  ("(var4 down)" 100 103)
  ("(var4 up)" 103 105)
  ("(var4 stable)" 105 107)
  ("(var4 up)" 107 109)
  ("(var4 stable)" 109 111)
  ("(var4 up)" 111 136)
  ("(var4 stable)" 136 391)
  ("(var1 stable)" 0 103)
  ("(var1 up)" 103 127)
  ("(var1 stable)" 127 129)
  ("(var1 up)" 129 134)
  ("(var1 stable)" 134 391)
  ("(var2 stable)" 0 118)
  ("(var2 up)" 118 120)
  ("(var2 down)" 120 125)
  ("(var2 stable)" 125 171)
  ("(var2 up)" 171 248)
  ("(var2 stable)" 248 391)
 )
)
(55
 (
  ("(var3 stable)" 0 81)
  ("(var3 up)" 81 109)
  ("(var3 stable)" 109 209)
  ("(var3 up)" 209 211)
  ("(var3 down)" 211 223)
  ("(var3 up)" 223 228)
  ("(var3 stable)" 228 368)
  ("(var4 stable)" 0 72)
  ("(var4 up)" 72 74)
  ("(var4 down)" 74 76)
  ("(var4 up)" 76 107)
  ("(var4 stable)" 107 368)
  ("(var1 stable)" 0 74)
  ("(var1 up)" 74 117)
  ("(var1 stable)" 117 368)
  ("(var2 stable)" 0 92)
  ("(var2 up)" 92 94)
  ("(var2 down)" 94 99)
  ("(var2 stable)" 99 148)
  ("(var2 up)" 148 231)
  ("(var2 stable)" 231 368)
 )
)
(56
 (
  ("(var3 stable)" 0 63)
  ("(var3 up)" 63 99)
  ("(var3 stable)" 99 165)
  ("(var3 up)" 165 172)
  ("(var3 down)" 172 180)
  ("(var3 stable)" 180 304)
  ("(var4 stable)" 0 67)
  ("(var4 up)" 67 95)
  ("(var4 stable)" 95 304)
  ("(var1 stable)" 0 65)
  ("(var1 up)" 65 91)
  ("(var1 stable)" 91 93)
  ("(var1 up)" 93 95)
  ("(var1 stable)" 95 100)
  ("(var1 up)" 100 102)
  ("(var1 stable)" 102 304)
  ("(var2 stable)" 0 80)
  ("(var2 up)" 80 82)
  ("(var2 down)" 82 89)
  ("(var2 up)" 89 186)
  ("(var2 stable)" 186 198)
  ("(var2 down)" 198 200)
  ("(var2 stable)" 200 304)
 )
)
(57
 (
  ("(var3 stable)" 0 27)
  ("(var3 up)" 27 59)
  ("(var3 stable)" 59 138)
  ("(var3 up)" 138 142)
  ("(var3 down)" 142 151)
  ("(var3 stable)" 151 153)
  ("(var3 up)" 153 159)
  ("(var3 stable)" 159 282)
  ("(var4 stable)" 0 31)
  ("(var4 up)" 31 62)
  ("(var4 stable)" 62 282)
  ("(var1 stable)" 0 29)
  ("(var1 up)" 29 63)
  ("(var1 stable)" 63 282)
  ("(var2 stable)" 0 46)
  ("(var2 up)" 46 48)
  ("(var2 down)" 48 53)
  ("(var2 stable)" 53 96)
  ("(var2 up)" 96 170)
  ("(var2 down)" 170 173)
  ("(var2 up)" 173 175)
  ("(var2 stable)" 175 282)
 )
)
(58
 (
  ("(var3 stable)" 0 39)
  ("(var3 up)" 39 41)
  ("(var3 stable)" 41 43)
  ("(var3 down)" 43 47)
  ("(var3 up)" 47 78)
  ("(var3 down)" 78 80)
  ("(var3 up)" 80 85)
  ("(var3 stable)" 85 170)
  ("(var3 up)" 170 177)
  ("(var3 down)" 177 187)
  ("(var3 up)" 187 192)
  ("(var3 down)" 192 194)
  ("(var3 stable)" 194 331)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 41)
  ("(var4 stable)" 41 45)
  ("(var4 up)" 45 83)
  ("(var4 down)" 83 85)
  ("(var4 stable)" 85 331)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 44)
  ("(var1 stable)" 44 49)
  ("(var1 up)" 49 82)
  ("(var1 stable)" 82 331)
  ("(var2 stable)" 0 64)
  ("(var2 up)" 64 68)
  ("(var2 down)" 68 74)
  ("(var2 up)" 74 186)
  ("(var2 stable)" 186 331)
 )
)
(59
 (
  ("(var3 stable)" 0 41)
  ("(var3 up)" 41 70)
  ("(var3 stable)" 70 156)
  ("(var3 up)" 156 162)
  ("(var3 down)" 162 171)
  ("(var3 up)" 171 176)
  ("(var3 stable)" 176 314)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 39)
  ("(var4 down)" 39 41)
  ("(var4 up)" 41 75)
  ("(var4 stable)" 75 314)
  ("(var1 stable)" 0 32)
  ("(var1 up)" 32 73)
  ("(var1 stable)" 73 314)
  ("(var2 stable)" 0 59)
  ("(var2 up)" 59 61)
  ("(var2 down)" 61 66)
  ("(var2 stable)" 66 108)
  ("(var2 up)" 108 188)
  ("(var2 stable)" 188 194)
  ("(var2 down)" 194 196)
  ("(var2 stable)" 196 314)
 )
)
(60
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 91)
  ("(var3 stable)" 91 93)
  ("(var3 up)" 93 98)
  ("(var3 stable)" 98 182)
  ("(var3 up)" 182 186)
  ("(var3 down)" 186 196)
  ("(var3 up)" 196 201)
  ("(var3 stable)" 201 345)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 93)
  ("(var4 stable)" 93 345)
  ("(var1 stable)" 0 63)
  ("(var1 up)" 63 65)
  ("(var1 stable)" 65 67)
  ("(var1 up)" 67 95)
  ("(var1 stable)" 95 345)
  ("(var2 stable)" 0 78)
  ("(var2 up)" 78 82)
  ("(var2 down)" 82 88)
  ("(var2 stable)" 88 123)
  ("(var2 up)" 123 202)
  ("(var2 down)" 202 204)
  ("(var2 up)" 204 206)
  ("(var2 stable)" 206 345)
 )
)
(61
 (
  ("(var3 stable)" 0 59)
  ("(var3 up)" 59 89)
  ("(var3 stable)" 89 165)
  ("(var3 up)" 165 168)
  ("(var3 stable)" 168 170)
  ("(var3 down)" 170 177)
  ("(var3 stable)" 177 179)
  ("(var3 up)" 179 182)
  ("(var3 stable)" 182 312)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 89)
  ("(var4 stable)" 89 312)
  ("(var1 stable)" 0 46)
  ("(var1 up)" 46 88)
  ("(var1 stable)" 88 312)
  ("(var2 stable)" 0 69)
  ("(var2 up)" 69 75)
  ("(var2 down)" 75 80)
  ("(var2 up)" 80 199)
  ("(var2 stable)" 199 312)
 )
)
(62
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 106)
  ("(var3 stable)" 106 109)
  ("(var3 up)" 109 111)
  ("(var3 stable)" 111 196)
  ("(var3 up)" 196 200)
  ("(var3 down)" 200 212)
  ("(var3 up)" 212 218)
  ("(var3 stable)" 218 361)
  ("(var4 stable)" 0 75)
  ("(var4 up)" 75 102)
  ("(var4 stable)" 102 104)
  ("(var4 up)" 104 106)
  ("(var4 stable)" 106 359)
  ("(var4 down)" 359 361)
  ("(var1 stable)" 0 77)
  ("(var1 up)" 77 112)
  ("(var1 stable)" 112 361)
  ("(var2 stable)" 0 92)
  ("(var2 up)" 92 95)
  ("(var2 down)" 95 99)
  ("(var2 stable)" 99 143)
  ("(var2 up)" 143 237)
  ("(var2 stable)" 237 361)
 )
)
(63
 (
  ("(var3 stable)" 0 50)
  ("(var3 up)" 50 78)
  ("(var3 stable)" 78 160)
  ("(var3 up)" 160 164)
  ("(var3 down)" 164 175)
  ("(var3 up)" 175 179)
  ("(var3 stable)" 179 314)
  ("(var4 stable)" 0 51)
  ("(var4 up)" 51 84)
  ("(var4 stable)" 84 314)
  ("(var1 stable)" 0 52)
  ("(var1 up)" 52 80)
  ("(var1 stable)" 80 314)
  ("(var2 stable)" 0 64)
  ("(var2 up)" 64 66)
  ("(var2 down)" 66 71)
  ("(var2 up)" 71 197)
  ("(var2 stable)" 197 314)
 )
)
(64
 (
  ("(var3 stable)" 0 36)
  ("(var3 down)" 36 38)
  ("(var3 up)" 38 63)
  ("(var3 stable)" 63 65)
  ("(var3 up)" 65 70)
  ("(var3 stable)" 70 148)
  ("(var3 up)" 148 153)
  ("(var3 down)" 153 164)
  ("(var3 up)" 164 168)
  ("(var3 stable)" 168 306)
  ("(var4 stable)" 0 27)
  ("(var4 up)" 27 65)
  ("(var4 stable)" 65 306)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 65)
  ("(var1 stable)" 65 306)
  ("(var2 stable)" 0 51)
  ("(var2 up)" 51 53)
  ("(var2 down)" 53 58)
  ("(var2 stable)" 58 99)
  ("(var2 up)" 99 163)
  ("(var2 down)" 163 165)
  ("(var2 stable)" 165 306)
 )
)
(65
 (
  ("(var3 stable)" 0 92)
  ("(var3 up)" 92 123)
  ("(var3 stable)" 123 204)
  ("(var3 up)" 204 210)
  ("(var3 down)" 210 219)
  ("(var3 up)" 219 222)
  ("(var3 stable)" 222 359)
  ("(var4 stable)" 0 95)
  ("(var4 up)" 95 124)
  ("(var4 stable)" 124 359)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 91)
  ("(var1 stable)" 91 93)
  ("(var1 up)" 93 122)
  ("(var1 stable)" 122 359)
  ("(var2 stable)" 0 106)
  ("(var2 up)" 106 108)
  ("(var2 down)" 108 113)
  ("(var2 stable)" 113 151)
  ("(var2 up)" 151 224)
  ("(var2 stable)" 224 359)
 )
)
(66
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 106)
  ("(var3 stable)" 106 190)
  ("(var3 up)" 190 193)
  ("(var3 down)" 193 205)
  ("(var3 up)" 205 209)
  ("(var3 stable)" 209 353)
  ("(var4 stable)" 0 67)
  ("(var4 up)" 67 101)
  ("(var4 stable)" 101 105)
  ("(var4 up)" 105 109)
  ("(var4 stable)" 109 353)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 101)
  ("(var1 stable)" 101 353)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 89)
  ("(var2 down)" 89 93)
  ("(var2 stable)" 93 140)
  ("(var2 up)" 140 207)
  ("(var2 stable)" 207 353)
 )
)
(67
 (
  ("(var3 stable)" 0 64)
  ("(var3 up)" 64 87)
  ("(var3 down)" 87 89)
  ("(var3 stable)" 89 168)
  ("(var3 up)" 168 172)
  ("(var3 down)" 172 181)
  ("(var3 up)" 181 187)
  ("(var3 stable)" 187 312)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 61)
  ("(var4 stable)" 61 63)
  ("(var4 up)" 63 88)
  ("(var4 stable)" 88 312)
  ("(var1 up)" 0 2)
  ("(var1 stable)" 2 60)
  ("(var1 up)" 60 62)
  ("(var1 stable)" 62 65)
  ("(var1 up)" 65 90)
  ("(var1 stable)" 90 312)
  ("(var2 stable)" 0 75)
  ("(var2 up)" 75 77)
  ("(var2 down)" 77 82)
  ("(var2 up)" 82 198)
  ("(var2 down)" 198 200)
  ("(var2 up)" 200 204)
  ("(var2 down)" 204 206)
  ("(var2 stable)" 206 312)
 )
)
(68
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 83)
  ("(var3 stable)" 83 163)
  ("(var3 up)" 163 165)
  ("(var3 down)" 165 175)
  ("(var3 up)" 175 180)
  ("(var3 stable)" 180 309)
  ("(var4 stable)" 0 50)
  ("(var4 up)" 50 82)
  ("(var4 stable)" 82 84)
  ("(var4 up)" 84 86)
  ("(var4 stable)" 86 309)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 85)
  ("(var1 stable)" 85 309)
  ("(var2 stable)" 0 67)
  ("(var2 up)" 67 69)
  ("(var2 down)" 69 74)
  ("(var2 stable)" 74 115)
  ("(var2 up)" 115 192)
  ("(var2 stable)" 192 309)
 )
)
(69
 (
  ("(var3 stable)" 0 37)
  ("(var3 up)" 37 69)
  ("(var3 stable)" 69 144)
  ("(var3 up)" 144 149)
  ("(var3 down)" 149 159)
  ("(var3 up)" 159 164)
  ("(var3 stable)" 164 293)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 63)
  ("(var4 stable)" 63 293)
  ("(var1 stable)" 0 37)
  ("(var1 up)" 37 65)
  ("(var1 stable)" 65 67)
  ("(var1 up)" 67 69)
  ("(var1 stable)" 69 293)
  ("(var2 stable)" 0 51)
  ("(var2 up)" 51 53)
  ("(var2 down)" 53 58)
  ("(var2 up)" 58 175)
  ("(var2 stable)" 175 293)
 )
)
(70
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 72)
  ("(var3 down)" 72 74)
  ("(var3 up)" 74 100)
  ("(var3 stable)" 100 176)
  ("(var3 up)" 176 181)
  ("(var3 down)" 181 190)
  ("(var3 stable)" 190 192)
  ("(var3 up)" 192 197)
  ("(var3 stable)" 197 329)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 103)
  ("(var4 stable)" 103 329)
  ("(var1 stable)" 0 70)
  ("(var1 up)" 70 99)
  ("(var1 stable)" 99 329)
  ("(var2 stable)" 0 84)
  ("(var2 up)" 84 88)
  ("(var2 down)" 88 90)
  ("(var2 up)" 90 210)
  ("(var2 stable)" 210 329)
 )
)
(71
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 86)
  ("(var3 stable)" 86 88)
  ("(var3 up)" 88 90)
  ("(var3 stable)" 90 174)
  ("(var3 up)" 174 178)
  ("(var3 down)" 178 188)
  ("(var3 up)" 188 195)
  ("(var3 stable)" 195 335)
  ("(var4 stable)" 0 46)
  ("(var4 up)" 46 92)
  ("(var4 stable)" 92 335)
  ("(var1 stable)" 0 51)
  ("(var1 up)" 51 95)
  ("(var1 stable)" 95 335)
  ("(var2 stable)" 0 73)
  ("(var2 up)" 73 77)
  ("(var2 down)" 77 81)
  ("(var2 stable)" 81 127)
  ("(var2 up)" 127 184)
  ("(var2 stable)" 184 186)
  ("(var2 up)" 186 189)
  ("(var2 stable)" 189 335)
 )
)
(72
 (
  ("(var3 stable)" 0 55)
  ("(var3 up)" 55 89)
  ("(var3 stable)" 89 177)
  ("(var3 up)" 177 182)
  ("(var3 down)" 182 191)
  ("(var3 up)" 191 196)
  ("(var3 stable)" 196 336)
  ("(var4 stable)" 0 57)
  ("(var4 up)" 57 91)
  ("(var4 stable)" 91 336)
  ("(var1 stable)" 0 53)
  ("(var1 up)" 53 93)
  ("(var1 down)" 93 95)
  ("(var1 stable)" 95 336)
  ("(var2 stable)" 0 71)
  ("(var2 up)" 71 73)
  ("(var2 down)" 73 78)
  ("(var2 stable)" 78 125)
  ("(var2 up)" 125 190)
  ("(var2 stable)" 190 336)
 )
)
(73
 (
  ("(var3 stable)" 0 92)
  ("(var3 up)" 92 122)
  ("(var3 stable)" 122 207)
  ("(var3 up)" 207 213)
  ("(var3 down)" 213 222)
  ("(var3 up)" 222 227)
  ("(var3 stable)" 227 367)
  ("(var4 stable)" 0 96)
  ("(var4 up)" 96 120)
  ("(var4 stable)" 120 367)
  ("(var1 stable)" 0 91)
  ("(var1 up)" 91 128)
  ("(var1 stable)" 128 367)
  ("(var2 stable)" 0 107)
  ("(var2 up)" 107 109)
  ("(var2 down)" 109 114)
  ("(var2 up)" 114 239)
  ("(var2 stable)" 239 367)
 )
)
(74
 (
  ("(var3 stable)" 0 61)
  ("(var3 down)" 61 63)
  ("(var3 up)" 63 68)
  ("(var3 down)" 68 71)
  ("(var3 up)" 71 104)
  ("(var3 stable)" 104 182)
  ("(var3 up)" 182 188)
  ("(var3 down)" 188 199)
  ("(var3 up)" 199 206)
  ("(var3 stable)" 206 353)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 98)
  ("(var4 stable)" 98 353)
  ("(var1 stable)" 0 68)
  ("(var1 up)" 68 98)
  ("(var1 stable)" 98 353)
  ("(var2 stable)" 0 83)
  ("(var2 up)" 83 85)
  ("(var2 down)" 85 90)
  ("(var2 stable)" 90 134)
  ("(var2 up)" 134 136)
  ("(var2 stable)" 136 138)
  ("(var2 up)" 138 218)
  ("(var2 stable)" 218 223)
  ("(var2 up)" 223 227)
  ("(var2 stable)" 227 353)
 )
)
(75
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 116)
  ("(var3 stable)" 116 196)
  ("(var3 up)" 196 203)
  ("(var3 down)" 203 214)
  ("(var3 up)" 214 217)
  ("(var3 stable)" 217 358)
  ("(var4 stable)" 0 80)
  ("(var4 up)" 80 109)
  ("(var4 stable)" 109 358)
  ("(var1 stable)" 0 78)
  ("(var1 up)" 78 115)
  ("(var1 stable)" 115 358)
  ("(var2 stable)" 0 97)
  ("(var2 up)" 97 99)
  ("(var2 down)" 99 104)
  ("(var2 up)" 104 245)
  ("(var2 stable)" 245 358)
 )
)
(76
 (
  ("(var3 stable)" 0 76)
  ("(var3 up)" 76 107)
  ("(var3 down)" 107 109)
  ("(var3 up)" 109 112)
  ("(var3 stable)" 112 187)
  ("(var3 up)" 187 189)
  ("(var3 down)" 189 199)
  ("(var3 up)" 199 201)
  ("(var3 stable)" 201 328)
  ("(var4 stable)" 0 79)
  ("(var4 up)" 79 111)
  ("(var4 stable)" 111 328)
  ("(var1 stable)" 0 82)
  ("(var1 up)" 82 108)
  ("(var1 stable)" 108 328)
  ("(var2 stable)" 0 99)
  ("(var2 down)" 99 101)
  ("(var2 stable)" 101 141)
  ("(var2 up)" 141 232)
  ("(var2 stable)" 232 328)
 )
)
(77
 (
  ("(var3 stable)" 0 58)
  ("(var3 up)" 58 97)
  ("(var3 stable)" 97 180)
  ("(var3 up)" 180 186)
  ("(var3 down)" 186 198)
  ("(var3 up)" 198 202)
  ("(var3 stable)" 202 343)
  ("(var4 stable)" 0 67)
  ("(var4 up)" 67 94)
  ("(var4 stable)" 94 343)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 92)
  ("(var1 stable)" 92 343)
  ("(var2 stable)" 0 77)
  ("(var2 up)" 77 81)
  ("(var2 down)" 81 85)
  ("(var2 up)" 85 239)
  ("(var2 stable)" 239 343)
 )
)
(78
 (
  ("(var3 stable)" 0 56)
  ("(var3 up)" 56 93)
  ("(var3 down)" 93 95)
  ("(var3 stable)" 95 176)
  ("(var3 up)" 176 181)
  ("(var3 down)" 181 190)
  ("(var3 up)" 190 196)
  ("(var3 stable)" 196 339)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 92)
  ("(var4 stable)" 92 339)
  ("(var1 stable)" 0 54)
  ("(var1 up)" 54 69)
  ("(var1 stable)" 69 71)
  ("(var1 up)" 71 86)
  ("(var1 stable)" 86 88)
  ("(var1 up)" 88 93)
  ("(var1 stable)" 93 339)
  ("(var2 stable)" 0 73)
  ("(var2 up)" 73 77)
  ("(var2 down)" 77 81)
  ("(var2 up)" 81 218)
  ("(var2 stable)" 218 339)
 )
)
(79
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 100)
  ("(var3 down)" 100 103)
  ("(var3 up)" 103 105)
  ("(var3 stable)" 105 185)
  ("(var3 up)" 185 190)
  ("(var3 down)" 190 202)
  ("(var3 up)" 202 207)
  ("(var3 stable)" 207 351)
  ("(var4 stable)" 0 72)
  ("(var4 up)" 72 98)
  ("(var4 stable)" 98 351)
  ("(var1 stable)" 0 69)
  ("(var1 up)" 69 72)
  ("(var1 stable)" 72 74)
  ("(var1 up)" 74 100)
  ("(var1 down)" 100 102)
  ("(var1 up)" 102 104)
  ("(var1 stable)" 104 351)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 87)
  ("(var2 down)" 87 92)
  ("(var2 stable)" 92 139)
  ("(var2 up)" 139 227)
  ("(var2 stable)" 227 351)
 )
)
(80
 (
  ("(var3 stable)" 0 78)
  ("(var3 up)" 78 112)
  ("(var3 stable)" 112 194)
  ("(var3 up)" 194 199)
  ("(var3 down)" 199 209)
  ("(var3 up)" 209 212)
  ("(var3 stable)" 212 350)
  ("(var4 stable)" 0 79)
  ("(var4 up)" 79 121)
  ("(var4 stable)" 121 350)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 75)
  ("(var1 stable)" 75 77)
  ("(var1 up)" 77 115)
  ("(var1 stable)" 115 350)
  ("(var2 stable)" 0 94)
  ("(var2 up)" 94 98)
  ("(var2 down)" 98 102)
  ("(var2 up)" 102 235)
  ("(var2 stable)" 235 350)
 )
)
(81
 (
  ("(var3 stable)" 0 71)
  ("(var3 up)" 71 73)
  ("(var3 down)" 73 75)
  ("(var3 up)" 75 102)
  ("(var3 stable)" 102 185)
  ("(var3 up)" 185 191)
  ("(var3 down)" 191 200)
  ("(var3 up)" 200 205)
  ("(var3 stable)" 205 340)
  ("(var4 stable)" 0 77)
  ("(var4 up)" 77 112)
  ("(var4 stable)" 112 340)
  ("(var1 stable)" 0 71)
  ("(var1 up)" 71 107)
  ("(var1 stable)" 107 340)
  ("(var2 stable)" 0 89)
  ("(var2 up)" 89 91)
  ("(var2 down)" 91 96)
  ("(var2 stable)" 96 138)
  ("(var2 up)" 138 236)
  ("(var2 stable)" 236 340)
 )
)
(82
 (
  ("(var3 stable)" 0 61)
  ("(var3 up)" 61 94)
  ("(var3 stable)" 94 164)
  ("(var3 up)" 164 168)
  ("(var3 down)" 168 180)
  ("(var3 up)" 180 182)
  ("(var3 stable)" 182 316)
  ("(var4 stable)" 0 61)
  ("(var4 up)" 61 95)
  ("(var4 stable)" 95 316)
  ("(var1 stable)" 0 62)
  ("(var1 up)" 62 91)
  ("(var1 stable)" 91 316)
  ("(var2 stable)" 0 75)
  ("(var2 up)" 75 77)
  ("(var2 down)" 77 82)
  ("(var2 up)" 82 171)
  ("(var2 stable)" 171 174)
  ("(var2 up)" 174 206)
  ("(var2 stable)" 206 316)
 )
)
(83
 (
  ("(var3 stable)" 0 53)
  ("(var3 down)" 53 55)
  ("(var3 up)" 55 88)
  ("(var3 stable)" 88 170)
  ("(var3 up)" 170 174)
  ("(var3 down)" 174 185)
  ("(var3 up)" 185 190)
  ("(var3 stable)" 190 326)
  ("(var4 stable)" 0 53)
  ("(var4 up)" 53 87)
  ("(var4 stable)" 87 326)
  ("(var1 stable)" 0 56)
  ("(var1 up)" 56 89)
  ("(var1 stable)" 89 326)
  ("(var2 stable)" 0 72)
  ("(var2 up)" 72 74)
  ("(var2 down)" 74 79)
  ("(var2 up)" 79 194)
  ("(var2 stable)" 194 326)
 )
)
(84
 (
  ("(var3 stable)" 0 32)
  ("(var3 up)" 32 36)
  ("(var3 stable)" 36 39)
  ("(var3 up)" 39 75)
  ("(var3 stable)" 75 155)
  ("(var3 up)" 155 159)
  ("(var3 stable)" 159 162)
  ("(var3 down)" 162 171)
  ("(var3 stable)" 171 173)
  ("(var3 up)" 173 177)
  ("(var3 stable)" 177 312)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 70)
  ("(var4 down)" 70 72)
  ("(var4 stable)" 72 312)
  ("(var1 stable)" 0 30)
  ("(var1 up)" 30 44)
  ("(var1 down)" 44 46)
  ("(var1 up)" 46 74)
  ("(var1 stable)" 74 312)
  ("(var2 stable)" 0 51)
  ("(var2 up)" 51 53)
  ("(var2 down)" 53 58)
  ("(var2 up)" 58 194)
  ("(var2 down)" 194 196)
  ("(var2 up)" 196 200)
  ("(var2 stable)" 200 312)
 )
)
(85
 (
  ("(var3 stable)" 0 30)
  ("(var3 up)" 30 63)
  ("(var3 stable)" 63 137)
  ("(var3 up)" 137 139)
  ("(var3 down)" 139 148)
  ("(var3 up)" 148 152)
  ("(var3 stable)" 152 279)
  ("(var4 stable)" 0 35)
  ("(var4 down)" 35 38)
  ("(var4 up)" 38 60)
  ("(var4 stable)" 60 279)
  ("(var1 stable)" 0 35)
  ("(var1 up)" 35 64)
  ("(var1 stable)" 64 279)
  ("(var2 stable)" 0 48)
  ("(var2 up)" 48 50)
  ("(var2 down)" 50 54)
  ("(var2 up)" 54 161)
  ("(var2 stable)" 161 279)
 )
)
(86
 (
  ("(var3 stable)" 0 67)
  ("(var3 up)" 67 103)
  ("(var3 stable)" 103 178)
  ("(var3 up)" 178 184)
  ("(var3 down)" 184 193)
  ("(var3 up)" 193 198)
  ("(var3 stable)" 198 331)
  ("(var4 stable)" 0 76)
  ("(var4 up)" 76 110)
  ("(var4 stable)" 110 331)
  ("(var1 stable)" 0 73)
  ("(var1 up)" 73 109)
  ("(var1 stable)" 109 331)
  ("(var2 stable)" 0 89)
  ("(var2 up)" 89 91)
  ("(var2 down)" 91 96)
  ("(var2 stable)" 96 135)
  ("(var2 up)" 135 230)
  ("(var2 stable)" 230 331)
 )
)
(87
 (
  ("(var3 stable)" 0 57)
  ("(var3 up)" 57 60)
  ("(var3 down)" 60 62)
  ("(var3 up)" 62 94)
  ("(var3 stable)" 94 181)
  ("(var3 up)" 181 190)
  ("(var3 down)" 190 199)
  ("(var3 up)" 199 206)
  ("(var3 stable)" 206 350)
  ("(var4 stable)" 0 64)
  ("(var4 up)" 64 66)
  ("(var4 down)" 66 68)
  ("(var4 up)" 68 97)
  ("(var4 stable)" 97 350)
  ("(var1 down)" 0 2)
  ("(var1 stable)" 2 58)
  ("(var1 up)" 58 97)
  ("(var1 stable)" 97 350)
  ("(var2 stable)" 0 78)
  ("(var2 up)" 78 82)
  ("(var2 down)" 82 87)
  ("(var2 up)" 87 139)
  ("(var2 stable)" 139 141)
  ("(var2 up)" 141 143)
  ("(var2 stable)" 143 145)
  ("(var2 up)" 145 181)
  ("(var2 down)" 181 183)
  ("(var2 up)" 183 221)
  ("(var2 stable)" 221 350)
 )
)
(88
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 66)
  ("(var3 down)" 66 68)
  ("(var3 stable)" 68 139)
  ("(var3 up)" 139 145)
  ("(var3 down)" 145 154)
  ("(var3 up)" 154 159)
  ("(var3 stable)" 159 288)
  ("(var4 stable)" 0 38)
  ("(var4 up)" 38 69)
  ("(var4 down)" 69 71)
  ("(var4 stable)" 71 288)
  ("(var1 stable)" 0 38)
  ("(var1 up)" 38 65)
  ("(var1 stable)" 65 67)
  ("(var1 up)" 67 69)
  ("(var1 stable)" 69 288)
  ("(var2 stable)" 0 52)
  ("(var2 up)" 52 54)
  ("(var2 down)" 54 58)
  ("(var2 stable)" 58 91)
  ("(var2 up)" 91 174)
  ("(var2 stable)" 174 288)
 )
)
(89
 (
  ("(var3 stable)" 0 70)
  ("(var3 up)" 70 95)
  ("(var3 stable)" 95 98)
  ("(var3 up)" 98 101)
  ("(var3 stable)" 101 175)
  ("(var3 up)" 175 182)
  ("(var3 down)" 182 192)
  ("(var3 up)" 192 196)
  ("(var3 stable)" 196 321)
  ("(var4 stable)" 0 69)
  ("(var4 up)" 69 101)
  ("(var4 stable)" 101 321)
  ("(var1 stable)" 0 67)
  ("(var1 up)" 67 97)
  ("(var1 stable)" 97 321)
  ("(var2 stable)" 0 82)
  ("(var2 up)" 82 84)
  ("(var2 down)" 84 89)
  ("(var2 up)" 89 128)
  ("(var2 stable)" 128 130)
  ("(var2 up)" 130 177)
  ("(var2 down)" 177 179)
  ("(var2 up)" 179 210)
  ("(var2 stable)" 210 321)
 )
)
(90
 (
  ("(var3 stable)" 0 57)
  ("(var3 up)" 57 82)
  ("(var3 stable)" 82 159)
  ("(var3 up)" 159 164)
  ("(var3 down)" 164 171)
  ("(var3 stable)" 171 307)
  ("(var4 stable)" 0 56)
  ("(var4 up)" 56 87)
  ("(var4 down)" 87 89)
  ("(var4 stable)" 89 307)
  ("(var1 stable)" 0 55)
  ("(var1 up)" 55 85)
  ("(var1 stable)" 85 307)
  ("(var2 stable)" 0 69)
  ("(var2 down)" 69 74)
  ("(var2 up)" 74 173)
  ("(var2 stable)" 173 307)
 )
)
(91
 (
  ("(var3 stable)" 0 69)
  ("(var3 up)" 69 104)
  ("(var3 stable)" 104 179)
  ("(var3 up)" 179 184)
  ("(var3 stable)" 184 186)
  ("(var3 down)" 186 194)
  ("(var3 up)" 194 199)
  ("(var3 stable)" 199 328)
  ("(var4 stable)" 0 73)
  ("(var4 up)" 73 101)
  ("(var4 down)" 101 103)
  ("(var4 stable)" 103 328)
  ("(var1 stable)" 0 71)
  ("(var1 up)" 71 100)
  ("(var1 stable)" 100 328)
  ("(var2 stable)" 0 85)
  ("(var2 up)" 85 87)
  ("(var2 down)" 87 92)
  ("(var2 up)" 92 227)
  ("(var2 stable)" 227 328)
 )
)
(92
 (
  ("(var3 stable)" 0 80)
  ("(var3 up)" 80 120)
  ("(var3 stable)" 120 203)
  ("(var3 up)" 203 208)
  ("(var3 down)" 208 217)
  ("(var3 stable)" 217 219)
  ("(var3 up)" 219 223)
  ("(var3 stable)" 223 370)
  ("(var4 stable)" 0 87)
  ("(var4 up)" 87 117)
  ("(var4 down)" 117 119)
  ("(var4 stable)" 119 370)
  ("(var1 stable)" 0 88)
  ("(var1 up)" 88 117)
  ("(var1 stable)" 117 370)
  ("(var2 stable)" 0 100)
  ("(var2 up)" 100 106)
  ("(var2 down)" 106 110)
  ("(var2 up)" 110 220)
  ("(var2 stable)" 220 370)
 )
)
(93
 (
  ("(var3 stable)" 0 38)
  ("(var3 up)" 38 40)
  ("(var3 down)" 40 42)
  ("(var3 up)" 42 76)
  ("(var3 stable)" 76 158)
  ("(var3 up)" 158 165)
  ("(var3 down)" 165 178)
  ("(var3 up)" 178 183)
  ("(var3 stable)" 183 327)
  ("(var4 stable)" 0 37)
  ("(var4 up)" 37 39)
  ("(var4 down)" 39 42)
  ("(var4 up)" 42 71)
  ("(var4 stable)" 71 327)
  ("(var1 stable)" 0 42)
  ("(var1 up)" 42 82)
  ("(var1 stable)" 82 327)
  ("(var2 stable)" 0 57)
  ("(var2 up)" 57 59)
  ("(var2 down)" 59 64)
  ("(var2 up)" 64 205)
  ("(var2 down)" 205 207)
  ("(var2 up)" 207 209)
  ("(var2 stable)" 209 327)
 )
)
(94
 (
  ("(var3 stable)" 0 51)
  ("(var3 up)" 51 85)
  ("(var3 stable)" 85 156)
  ("(var3 up)" 156 161)
  ("(var3 down)" 161 171)
  ("(var3 up)" 171 173)
  ("(var3 stable)" 173 296)
  ("(var4 stable)" 0 47)
  ("(var4 up)" 47 86)
  ("(var4 stable)" 86 296)
  ("(var1 stable)" 0 45)
  ("(var1 up)" 45 85)
  ("(var1 stable)" 85 296)
  ("(var2 stable)" 0 67)
  ("(var2 up)" 67 69)
  ("(var2 down)" 69 74)
  ("(var2 up)" 74 187)
  ("(var2 stable)" 187 296)
 )
)
(95
 (
  ("(var3 stable)" 0 90)
  ("(var3 up)" 90 122)
  ("(var3 down)" 122 127)
  ("(var3 up)" 127 129)
  ("(var3 stable)" 129 199)
  ("(var3 up)" 199 206)
  ("(var3 down)" 206 216)
  ("(var3 up)" 216 221)
  ("(var3 stable)" 221 363)
  ("(var4 stable)" 0 85)
  ("(var4 up)" 85 90)
  ("(var4 stable)" 90 92)
  ("(var4 up)" 92 120)
  ("(var4 stable)" 120 363)
  ("(var1 stable)" 0 87)
  ("(var1 up)" 87 115)
  ("(var1 down)" 115 117)
  ("(var1 up)" 117 122)
  ("(var1 stable)" 122 363)
  ("(var2 stable)" 0 103)
  ("(var2 up)" 103 105)
  ("(var2 down)" 105 110)
  ("(var2 up)" 110 233)
  ("(var2 down)" 233 235)
  ("(var2 up)" 235 243)
  ("(var2 stable)" 243 363)
 )
)
(96
 (
  ("(var3 stable)" 0 62)
  ("(var3 up)" 62 104)
  ("(var3 stable)" 104 179)
  ("(var3 up)" 179 183)
  ("(var3 stable)" 183 185)
  ("(var3 down)" 185 194)
  ("(var3 up)" 194 200)
  ("(var3 stable)" 200 334)
  ("(var4 stable)" 0 70)
  ("(var4 up)" 70 97)
  ("(var4 stable)" 97 334)
  ("(var1 stable)" 0 66)
  ("(var1 up)" 66 101)
  ("(var1 stable)" 101 334)
  ("(var2 stable)" 0 83)
  ("(var2 up)" 83 85)
  ("(var2 down)" 85 90)
  ("(var2 up)" 90 212)
  ("(var2 down)" 212 214)
  ("(var2 up)" 214 217)
  ("(var2 stable)" 217 334)
 )
)
(97
 (
  ("(var3 stable)" 0 96)
  ("(var3 up)" 96 126)
  ("(var3 stable)" 126 219)
  ("(var3 up)" 219 223)
  ("(var3 stable)" 223 225)
  ("(var3 down)" 225 235)
  ("(var3 stable)" 235 238)
  ("(var3 up)" 238 243)
  ("(var3 stable)" 243 385)
  ("(var4 down)" 0 2)
  ("(var4 up)" 2 4)
  ("(var4 stable)" 4 93)
  ("(var4 up)" 93 117)
  ("(var4 stable)" 117 119)
  ("(var4 up)" 119 125)
  ("(var4 stable)" 125 385)
  ("(var1 stable)" 0 98)
  ("(var1 up)" 98 128)
  ("(var1 stable)" 128 385)
  ("(var2 stable)" 0 110)
  ("(var2 up)" 110 112)
  ("(var2 down)" 112 121)
  ("(var2 up)" 121 164)
  ("(var2 stable)" 164 166)
  ("(var2 down)" 166 168)
  ("(var2 up)" 168 225)
  ("(var2 down)" 225 227)
  ("(var2 up)" 227 229)
  ("(var2 down)" 229 231)
  ("(var2 up)" 231 258)
  ("(var2 stable)" 258 385)
 )
)
(98
 (
  ("(var3 stable)" 0 90)
  ("(var3 up)" 90 125)
  ("(var3 stable)" 125 205)
  ("(var3 up)" 205 208)
  ("(var3 stable)" 208 210)
  ("(var3 down)" 210 218)
  ("(var3 stable)" 218 221)
  ("(var3 up)" 221 226)
  ("(var3 stable)" 226 361)
  ("(var4 stable)" 0 86)
  ("(var4 up)" 86 127)
  ("(var4 stable)" 127 361)
  ("(var1 stable)" 0 92)
  ("(var1 up)" 92 126)
  ("(var1 stable)" 126 361)
  ("(var2 stable)" 0 107)
  ("(var2 up)" 107 109)
  ("(var2 down)" 109 114)
  ("(var2 up)" 114 250)
  ("(var2 stable)" 250 361)
 )
)
(99
 (
  ("(var3 stable)" 0 91)
  ("(var3 up)" 91 123)
  ("(var3 stable)" 123 201)
  ("(var3 up)" 201 207)
  ("(var3 down)" 207 216)
  ("(var3 stable)" 216 218)
  ("(var3 up)" 218 223)
  ("(var3 stable)" 223 359)
  ("(var4 stable)" 0 93)
  ("(var4 up)" 93 122)
  ("(var4 down)" 122 125)
  ("(var4 up)" 125 127)
  ("(var4 stable)" 127 359)
  ("(var1 stable)" 0 86)
  ("(var1 up)" 86 119)
  ("(var1 down)" 119 121)
  ("(var1 up)" 121 123)
  ("(var1 stable)" 123 359)
  ("(var2 stable)" 0 104)
  ("(var2 up)" 104 106)
  ("(var2 down)" 106 111)
  ("(var2 up)" 111 238)
  ("(var2 down)" 238 240)
  ("(var2 stable)" 240 359)
 )
)
(100
 (
  ("(var3 stable)" 0 60)
  ("(var3 up)" 60 85)
  ("(var3 stable)" 85 87)
  ("(var3 up)" 87 101)
  ("(var3 stable)" 101 180)
  ("(var3 up)" 180 185)
  ("(var3 stable)" 185 187)
  ("(var3 down)" 187 200)
  ("(var3 up)" 200 203)
  ("(var3 stable)" 203 353)
  ("(var4 stable)" 0 59)
  ("(var4 up)" 59 86)
  ("(var4 down)" 86 88)
  ("(var4 up)" 88 90)
  ("(var4 stable)" 90 93)
  ("(var4 up)" 93 95)
  ("(var4 stable)" 95 353)
  ("(var1 stable)" 0 61)
  ("(var1 up)" 61 92)
  ("(var1 stable)" 92 353)
  ("(var2 stable)" 0 76)
  ("(var2 up)" 76 78)
  ("(var2 down)" 78 83)
  ("(var2 up)" 83 140)
  ("(var2 stable)" 140 142)
  ("(var2 up)" 142 213)
  ("(var2 stable)" 213 353)
 )
)
